Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New capture escape checking based on levels #18463

Merged
merged 76 commits into from
Sep 9, 2023

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Aug 27, 2023

A new scope restriction scheme for capture checking based on levels.

The idea is to have a stack of capture roots where inner capture roots are super-captures of outer roots.

Refines and supersedes #18348

This was overlooked before.
This demonstrates currently unsoundness when it comes to assignments via setters
There was a corner case in installAfter where

 - A denotation valid in a single phase got replaced by another one
 - Immediately after, the symbol's denotation would be forced in a previous phase

This somehow landed on a wrong denotation. The problem got apparent when more symbols
underwent a Recheck.updateInfoBetween. The flags field installed by a previous update
somehow was not recognized anymore. Specifically, the following was observed in order:

 1. For a parameter getter (xs in LazyList, file pos-custeom-args/captures/lazylists1.scala)
   the Private flag was suppressed via transformInfo at phase cc.
 2. The denotation of the getter v which was valid in the single phase cc+1 was updated at
    at cc by updateInfoInBetween in Recheck so that the Private flag was re-asserted in cc+1.
 3. Immediately afterwards, the getter's flags was demanded at phase cc.
 4. The Private flag was present, even though it should not be.

The problem was fixed by demanding the denotation of the getter as part of isntallAfter.
Constrain closure parameters and result from expected type before rechecking the closure's
body. This gives more precise types and avoids the spurious duplication of some
variables.

It also avoids the unmotivated special case that we needed before to make tests pass.
Previously, the result of a map could contain duplicates.

I verified that with the current code base this could cause problems only for
capture checking.
This reduces the chance of information loss in capture set
propagation for applications.
Currently not needed (was needed for level checking in other branch),
but kept since it is a useful generalization.
These changes were needed if we wanted to map all capability classes C to C^.
They are a good idea anyway since they make the mapping more robust.
 - Define a notion of ccNestingLevel, which corresponds to the nesting level
   of so called "level owners" relative to each other.
 - The outermost level owner is _root_.
 - Other level owners are classes that are not staticOwners
   and methods that are not constructors.
 - The ccNestingLevel of any symbol is the ccNestingLevel of its closest enclosing
   level owner, or -1 for NoSymbol.
 - Capture set variables are created with a level owner.
 - Capture set variables cannot include elements with higher ccNestingLevels
   than the variable's owner.
 - If level-incorrect elements are attempted to be added to a capture set variable,
   they are instead widened to the underlying capture set.
 - Use addenda mechanism to report level errors
Previously, the ccState property was missing on the context used for printing at phase cc.
Intended as a stop-gap for some (as-seen-from related?) problems
when comparing capture refinements of classes.
Copy link
Contributor

@Linyxus Linyxus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise LGTM!

Comment on lines 466 to 467
// infos other methods are determined from their definitions which
// are checked on depand
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// infos other methods are determined from their definitions which
// are checked on depand
// infos of other methods are determined from their definitions which
// are checked on demand

val y1 = f(x1.asInstanceOf[Elem])
val y2 = f(x2.asInstanceOf[Elem])
if (y0 ne y1) && (y0 ne y2) && (y1 ne y2) then Set3(y0, y1, y2)
else super.map(f)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This results in computing f again over each element, maybe:

Suggested change
else super.map(f)
else Set(y0, y1, y2)

recur(to, from)
case _ =>
mapOver(t)
def inverse = thisMap
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it a typo? It seems that the lazyval inverse should be returned here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, the inverse of the inverse is thisMap .

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes, sorry for the false alarm.

mapOverFollowingAliases(t)

private def transformExplicitType(tp: Type, boxed: Boolean, mapRoots: Boolean)(using Context): Type =
val tp1 = expandAliases(if boxed then box(tp) else tp)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems better to first expandAliases (or, at least, expandCapabilityClass) then box the type. Say, if we are transforming an explicit mention of a capability class (say, IO) in a type application, the correct outcome should be box IO^. The box should be there because the capability class is impure. Right now this isn't happening: the output is simply IO^. This is because we are boxing it before expanding, so the original IO isn't recognized as something to be boxed.

I found an unsound example which hides the usage of a capability:

  @capability class CanIO { def use(): Unit = () }
  def use[X](x: X): (op: X -> Unit) -> Unit = op => op(x)
  def test(io: CanIO): Unit =
    val f = use[CanIO](io)
    val g: () -> Unit = () => f(x => x.use())
    // UNSOUND: g uses the capability io but has an empty capture set

end isEnclosingRoot
end CaptureRoot

//class LevelError(val rvar: RootVar, val newBound: Symbol, val isUpper: Boolean) extends Exception
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LevelError doesn't seem to be used any more. Is the comment intentionally kept?

else false

/** The owner of the current level. Qualifying owners are
* - methods other than constructors and anonymous functions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
* - methods other than constructors and anonymous functions
* - methods other than constructors, anonymous functions, and synthetic case class accessors

Comment on lines 827 to 832
/** An extractor for eta expanded `mdef` an eta-expansion of a method reference? To recognize this, we use
* the following criterion: A method definition is an eta expansion, if
* it contains at least one term paramter, the parameter has a zero extent span,
* and the right hand side is either an application or a closure with'
* an anonymous method that's itself characterized as an eta expansion.
*/
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
/** An extractor for eta expanded `mdef` an eta-expansion of a method reference? To recognize this, we use
* the following criterion: A method definition is an eta expansion, if
* it contains at least one term paramter, the parameter has a zero extent span,
* and the right hand side is either an application or a closure with'
* an anonymous method that's itself characterized as an eta expansion.
*/
/** An extractor for eta expanded `mdef` or an eta-expansion of a method reference. To recognize this, we use
* the following criterion: A method definition is an eta expansion, if
* it contains at least one term paramter, the parameter has a zero extent span,
* and the right hand side is either an application or a closure with
* an anonymous method that's itself characterized as an eta expansion.
*/

Some refined function types are of the form

    (A->B)^{cs} { def apply(x: A): B' = ... }

In this case the capture set `cs` was previously dropped. Now it is printed.
Do it in setup instead of on demand. Advantage: no need to determine
level ownership for externally compiled symbols.
@odersky odersky merged commit 64c3138 into scala:main Sep 9, 2023
17 checks passed
@odersky odersky deleted the add-root-levels branch September 9, 2023 10:55
odersky added a commit to dotty-staging/dotty that referenced this pull request Oct 12, 2023
This reverts commit 64c3138, reversing
changes made to 08f2faf.

# Conflicts:
#	compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
#	compiler/src/dotty/tools/dotc/cc/Setup.scala
#	compiler/src/dotty/tools/dotc/transform/Recheck.scala
@Kordyjan Kordyjan added this to the 3.4.0 milestone Dec 20, 2023
WojciechMazur added a commit to WojciechMazur/dotty that referenced this pull request May 29, 2024
WojciechMazur added a commit to WojciechMazur/dotty that referenced this pull request Jun 14, 2024
WojciechMazur added a commit to WojciechMazur/dotty that referenced this pull request Jun 14, 2024
WojciechMazur added a commit that referenced this pull request Jun 17, 2024
WojciechMazur added a commit to WojciechMazur/dotty that referenced this pull request Jul 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants